Nuprl Lemma : q_less_wf 11,40
a, b:. q_less(a;b)   
latex

Definitionst.1, gset, |g|, |p|, <+>, goset, q_less(a;b), t  T, x:A. B(x), Mon, AbMon, OCMon, OGrp
Lemmasrationals wf, ocgrp wf, qadd grp wf2, oset of ocmon wf0, set blt wf

origin